
public abstract class Seg {
	
	static /*@ spec_public @*/ int num_inst;
	
	//ids de todos os seg que sao next de algum seg
	static /*@ spec_public @*/ int[] nexts;
	static /*@ spec_public @*/ int n;
	
	//@ invariant n == nexts.length && nexts != null;
	
	public int id;
	
	//Regra 4 (parte 1/2).	
	//@ invariant this != this.next; 
	public Seg next;
	
	//Regra 1.
	public Semaphore sema;
	
	public Seg() {
		id=num_inst;
		num_inst++;
		next=null;
		sema=null;
	}
	
	//Regra 3.
	//@ requires (\forall int i; i >= 0 && i < nexts.length ; nexts[i] != n_next.id) ;
	//@ requires n < nexts.length;
	public Seg(Seg n_next, Semaphore n_sema) {
		id=num_inst;
		num_inst++;
		this.next=n_next;
		this.sema=n_sema;
		//if (n_next != null ) nexts[n++]= n_next.getId();
		
	}
	
	//@ requires s != null && n < nexts.length;
	public Seg(Seg s) {
		id=num_inst;
		num_inst++;
		this.next=s.next;
		this.sema=s.sema;
		//if (s.next != null ) nexts[n++] = s.next.getId();
	}
	
	public /*@pure @*/ Seg getNext() {
		return next;
	}

	//@ requires next != this;
	public void setNext(Seg next) {
		this.next = next;
	}

	public Semaphore getSema() {
		return sema;
	}

	public void setSema(Semaphore sema) {
		this.sema = sema;
	}

	public static int getNum_inst() {
		return num_inst;
	}

	public int getId() {
		return id;
	}
	
}
